; EXPECT: unsat
(set-option :incremental false)
(set-logic ALL)
(declare-sort Atom 0)



(declare-fun Target () (Relation Atom))
(declare-fun Name () (Relation Atom))
(declare-fun Addr () (Relation Atom))
(declare-fun Book () (Relation Atom))
(declare-fun names () (Relation Atom Atom))
(declare-fun addr () (Relation Atom Atom Atom))
(declare-fun b1 () Atom)
(declare-fun b1_tup () (Tuple Atom))
(assert (= b1_tup (tuple b1)))
(assert (set.member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
(assert (= b2_tup (tuple b2)))
(assert (set.member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
(assert (= b3_tup (tuple b3)))
(assert (set.member b3_tup Book))
(declare-fun n () Atom)
(declare-fun n_tup () (Tuple Atom))
(assert (= n_tup (tuple n)))
(assert (set.member n_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
(assert (= t_tup (tuple t)))
(assert (set.member t_tup Target))
(assert (set.subset (rel.join (rel.join Book addr) Target) Name))
(assert (set.subset (rel.join Book names) Name))
(assert (= (set.inter Name Addr) (as set.empty (Relation Atom))))
(assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Relation Atom))))
(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup)))))
(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup)))))
(assert (let ((_let_1 (set.singleton n_tup))) (not (= (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (rel.join _let_1 (rel.join (set.singleton b3_tup) addr))))))
(check-sat)
